Exploration
Accueil
Racine
Exploration
Accueil
Racine

Serveur d'exploration sur la recherche en informatique en Lorraine

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

Specification and Refinement of Mobile Systems in MTLA and Mobile UML

Identifieur interne : 005E22 ( Main/Exploration ); précédent : 005E21; suivant : 005E23

Specification and Refinement of Mobile Systems in MTLA and Mobile UML

Auteurs : Alexander Knapp ; Stephan Merz ; Martin Wirsing ; Julia Zappe

Source :

RBID : CRIN:knapp05a

English descriptors

Abstract

We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the Mobile UML notation. We identify refinement principles for mobile systems and justify refinements of Mobile UML state machines with the help of the MTLA semantics.


Affiliations:

Links toward previous steps (curation, corpus...)

Le document en format XML

<record>
<TEI>
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en" wicri:score="394">Specification and Refinement of Mobile Systems in MTLA and Mobile UML</title>
</titleStmt>
<publicationStmt>
<idno type="RBID">CRIN:knapp05a</idno>
<date when="2005" year="2005">2005</date>
<idno type="wicri:Area/Crin/Corpus">004421</idno>
<idno type="wicri:Area/Crin/Curation">004421</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004421</idno>
<idno type="wicri:Area/Crin/Checkpoint">000270</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000270</idno>
<idno type="wicri:Area/Main/Merge">006045</idno>
<idno type="wicri:Area/Main/Curation">005E22</idno>
<idno type="wicri:Area/Main/Exploration">005E22</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title xml:lang="en">Specification and Refinement of Mobile Systems in MTLA and Mobile UML</title>
<author>
<name sortKey="Knapp, Alexander" sort="Knapp, Alexander" uniqKey="Knapp A" first="Alexander" last="Knapp">Alexander Knapp</name>
</author>
<author>
<name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
</author>
<author>
<name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name>
</author>
<author>
<name sortKey="Zappe, Julia" sort="Zappe, Julia" uniqKey="Zappe J" first="Julia" last="Zappe">Julia Zappe</name>
</author>
</analytic>
<series>
<title level="j">Theoretical Computer Science</title>
<imprint>
<date when="2005" type="published">2005</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc>
<textClass>
<keywords scheme="KwdEn" xml:lang="en">
<term>UML</term>
<term>mobile systems</term>
<term>refinement</term>
<term>spatial logic</term>
<term>specification</term>
<term>system development</term>
<term>temporal logic</term>
<term>verification</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en" wicri:score="1711">We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the Mobile UML notation. We identify refinement principles for mobile systems and justify refinements of Mobile UML state machines with the help of the MTLA semantics.</div>
</front>
</TEI>
<affiliations>
<list></list>
<tree>
<noCountry>
<name sortKey="Knapp, Alexander" sort="Knapp, Alexander" uniqKey="Knapp A" first="Alexander" last="Knapp">Alexander Knapp</name>
<name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
<name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name>
<name sortKey="Zappe, Julia" sort="Zappe, Julia" uniqKey="Zappe J" first="Julia" last="Zappe">Julia Zappe</name>
</noCountry>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005E22 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005E22 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     CRIN:knapp05a
   |texte=   Specification and Refinement of Mobile Systems in MTLA and Mobile UML
}}
Wicri

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022